The present invention relates to a method and system for processing information, and, more particularly, to a method and system for processing information providing the following distinctive features:                the system is able to interact, via appropriate interface devices, with a wide variety of clients, including humans, computers, computer networks, and systems like itself;        the system is capable of adopting an unlimited set of languages, both natural and artificial, to be used in communicating with the external world;        all kinds of system input information, including definitions of new languages, can be presented in any currently adopted language having the capability of expressing that information (the system is capable of adopting a wide variety of languages, including languages of limited expressive capability, which may serve specialized purposes, and thus may not be suitable for the purpose of language definition);        the system is able to find, from previously processed and stored information, full, precise and specific answers to relevant questions;        a system response can be presented in any of the currently adopted languages according to the desire of the client, provided, as discussed above, that that particular language is capable of expressing that response (responses that cannot be expressed in the desired language are handled according to error-handling rules that may be dynamically modified to suit the needs of the client);        the system is able to automatically extend the lexicon of an adopted language when encountering new terms in a known context;        the system is able to fully store input information even in cases where that information includes currently incomprehensible fragments, those fragments being made comprehensible later by the system acquiring further knowledge.        
These features are useful in applications in various industrial, commercial, social, scientific and educational domains, especially those characterized by:                availability of massive non-structured (textual) sources of information (such as catalogs, manuals, encyclopedias and codes of rules) and a necessity to provide effective extraction of precise and specific answers to particular questions;        necessity to provide easy and shared access to informational resources by wide communities of clients having no specialized knowledge of database systems, without preliminary training, and possibly speaking different languages;        necessity to merge and share knowledge and information stored in multiple informational systems created separately and specialized in different areas, for example, Product Design Management (PDM) and Enterprise Resource Planning (ERP) systems of large corporations, or information systems of separate government services;        necessity for automatic analysis, classification, referencing and translation of textual information (as in editorial and publishing houses).        
The present invention makes use of Sorted-Type Theory. See for example, Daniel Gallin, Intensional and Higher-Order Modal Logic, North Holland Publishing Company (an imprint of American Elsevier Publishing Company), Amsterdam, 1975, ASIN: 044411002X, which is incorporated by reference for all purposes as if fully set forth herein. See also, for example, B. Carpenter, Type-logical Semantics, MIT Press, Cambridge, Mass., 1997, ISBN: 0262531496, which is incorporated by reference for all purposes as if fully set forth herein. A brief introduction to sorted-type theory follows:
A.1) Tyn language:
Basic concepts of any type theory are types and terms. In the n-sorted-type theory there are n+1 primitive types:                t—truth type        e1, e2, . . . en—types of entities (or individuals) of n different sortsand an infinite set of derived (functional) types which are built as ordered pairs of types, that is, if a and b are types, then (ab) is also a type.        
For example, using the synonyms e,f, and g for e1, e2,, and e3,, respectively, (et), t(ef), ((et)g) and (((et))(tg)) are all derived types of Ty3. For the sake of brevity, we will omit below parentheses in functional types unless they are required to express pairing in an order other than from right to left, i.e., the types of this example would be written as: et, tef, (et)g, and ((et)f)tg.
Terms of Tyn are characterized recursively:
primitive terms of type a are variables xa0, xa1, xa2, . . . and constants Ca0, Ca1, Ca2 . . . (the first three variables of type a will be also denoted by synonymous symbols xa, ya, za);
derived terms are built by means of the three fundamental operations of Tyn:
if Y is a term of type ab and X is a term of type a, then application Y X is a term of type b;
if Y is a term of type b, then lambda abstraction λxakY is a term of type ab;
if X and Y are terms of type a, then equality X=Y is a term of type t.
Examples of Ty3 terms include: xe1, C(et)f12, C(et)f12xet4, λxet4cf6, xef2=Cef0, and Cte5(Cgf1=λxgCf9).
Below, important notions of free and bound occurrence of a variable in a term are used: an occurrence of a variable xb in a term Aa is bound if it occurs only within a part like λxbBc, otherwise it is said to be free.
All simpler terms incoming as constituents into a derived term (except bound variables) are said to be its sub-terms. For example, sub-terms of an application YX or an equality X=Y are X, Y and all sub-terms of X and Y (recursively); sub-terms of λxakY are Y and all its sub-terms. We will denote the fact that a term B is a sub-term of A with the notation A(B).
Given a term A(xa) and a term B, we say that B is free for xa in A(xa) if no free occurrence of xa in A(xa)lies within a part λybC, where yb occurs free in B. In other words, B is free for xa in A(xa) if and only if no one of free variables of B proves to be bound when B replaces all free occurrences of xa in A.
A.2) Tyn Semantics:
Exploring now the meaning of Tyn terms, consider n arbitrary (but non-empty) sets M1, M2, . . . Mn and also a special set 2={0, 1} (note the underlining which serves to distinguish this notation from the numeral 2). Let us associate with any type a some set Ma defined recursively as follows:
Mt=2, Me=M1, Mf=M2, and so on,                Mab=Mb^Ma that denotes a set of functions from Ma to Mb.        
Let any constant of type a represent a certain element of Ma, and any variable of type a represent an arbitrary (“unknown”) element of Ma. Then we can (again recursively) specify what is represented by any term:
Y X represents the result of the application of function [Y] to argument [X], where [Aa] denotes an element of Ma represented by a term;
λxakY represents the function from Mab whose value for any X from Ma is equal to [Y](xak/X), where [Y](xak/X ), denotes that element of Mb which is represented by Y, subject to the condition that [xak]=X;
X=Y represents 1 if [X]=[Y] and 0 otherwise.
Thus, having assigned each Tyn constant Cak an element [Cak] of a corresponding set Ma, we can find an element [A] of a corresponding set for any given term A and for any given assignment to the Tyn variables. A mapping M: Cak→[Cak] (for given sets M1, M2, . . . Mn) is said to be a model of Tyn based on M1, M2, . . . Mn.
Now, a few new, simple but important definitions:                a formula of Tyn is any term of type t;        a formula A is said to be true in a model if in this model [A]=1 for any assignment to the variables;        a set G of formulas is said to be satisfied in a model if every formula from G is true in that model;        a set G of formulas is said to be satisfiable if there is at least one model in which G is satisfied;        a formula A is said to be a semantic consequence of a set G of formulas (which fact is denoted as G|=A) if A is true whenever G is satisfied.        
Informally, the above construction can be interpreted as follows: ei-terms (that is, terms of type ei) represent entities of the i-th sort (either constant or depending on some variable objects) and t-terms represent truth values (also either constant or depending on some variable objects); ab-terms generally represent functions from a-objects to b-objects, for example, at-terms represent predicates about a-objects.
It is easy to check that the formulas:T≡(λxtxt=λxtxt)F≡(λxtxt=λxtT)(where the sign “≡” serves to introduce synonymous notations) in any model are represented by 1 and 0, correspondingly; that is why they define regular “true” and “false” sentences of the first-order logic. Similarly the regular sentential connectives and quantifiers can be defined:                ˜≡λxt(F=xt) (negation)        ≡λxtλyt(λf(tt)(fx=y)=λf(tt)(fT)) (conjunction)        →≡λxtλyt((xy)=x) (implication)        ≡λxtλyt(˜x→y) (disjunction)        ∀xaY≡(λxaY=λxaT) (generality quantifier)        ∃xaY≡˜∀xa˜Y (existence quantifier)A.3) Tyn Logic:        
The power of Tyn (as well as of any other formal theory) is revealed by the fact that it is sufficient to supply a very short list of some special formulas (referred to as axioms) and inference rules in order to be able to obtain potentially infinite set of formulas which will be true in any model.
Following is the list of axioms of Tyn:fttTfttF=Axt(fttxt)  1.xa=ya→fatxa=fatya  2.Axa(fabxa=gabxa)=(fab=gab)  3.(λxaAb(xa))Ba=Ab(Ba)  4.
where Ab(Ba) comes from Ab(xa) by replacing all free occurrences of xa by the term Ba, and Ba is free for xa in A(xa).
Tyn has a single inference rule:                1. from Aa=A′a and the formula B to infer the formula B′ which comes from B by replacing one occurrence of Aa (not immediately preceded by λ) by the term A′a.        
A proof in Tyn is a sequence of formulas each of which is either an axiom or else is obtained from earlier formulas by the inference rule. A formula A is said to be provable or a theorem of Tyn, which fact is denoted as |−A, if there is a proof in which A is the last formula.
A formula A is said to be derivable from a set G of formulas if it is provable in Tyn supplied with all formulas from G as additional axioms, which fact is denoted as G |−A. A set G of formulas is said to be consistent if F is not derivable from G. Finally, if |−˜A, then A is said to be refutable; we also say that A is refutable by G if G |−˜A. It is easy to prove that, if A is refutable by G, then G {A} is inconsistent.
Now we are ready to formulate the two fundamental facts:                G|−A implies G|=A in all models (Soundness Theorem)        G|=A in all models implies G|−A (Completeness Theorem)        
A final note: it is not to be supposed that any particular formula is either provable or refutable in Tyn: in fact there is an infinite number of formulas that are neither provable nor refutable. This important fact allows extensions to the set of the common Tyn axioms by infinitely large consistent sets of additional, specific axioms. A theory obtained as the result of such an expansion of the axiom set is said to be a restriction of Tyn because the sets of provable and refutable formulas for the new theory, of course, contain more formulas.
Various attempts have been made to provide systems that process information in a variety of natural languages. U.S. Pat. No. 6,182,062 presents a system that coexistently stores information in a variety of languages. In this approach, the amount of storage needed increases in proportion to the number of languages. There is thus a widely recognized need for, and it would be highly advantageous to have, an information processing system able to communicate in a variety of natural and artificial languages, adopt new languages, store information in a single internal representation, and respond to requests for information in a language chosen by the client.